Nuprl Lemma : grp_op_preserves_le
13,42
postcript
pdf
g
:OCMon,
x
,
y
,
z
:|
g
|. (
y
z
)
((
x
*
y
)
(
x
*
z
))
latex
Up
groups
1
Definitions of Statement
a
b
Definitions
monot(
T
;
x
,
y
.
R
(
x
;
y
);
f
)
,
a
b
Lemmas
ocmon
6
origin
g:OCMon, x, y, z:|g|. (y 
z) 
((x * y) (x * z)) g:OCMon, x, y, z:|g|. (y z) ((x * y) (x * z)) b b